

LEMMA

If x is externally connected to y and y is a non-tangential proper part of z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (ec c545479 c545478)) v (~ (ntpp c545478 c545477))) v (~ (p c545477 c545479)))


> hypdisj
=============================
Step 3

? (~ (p c545477 c545479))

1. (ntpp c545478 c545477)
2. (ec c545479 c545478)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var70 c545477)
|
|1. (p c545477 c545479)
|2. (ntpp c545478 c545477)
|3. (ec c545479 c545478)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var73 c545477)
||
||1. (~ (c Var70 c545477))
||2. (p c545477 c545479)
||3. (ntpp c545478 c545477)
||4. (ec c545479 c545478)
||
||> ((p Z X) <-- (~ (c (f540426 Z X Y) Z)))
||=============================
||Step 6
||
||? (~ (c (f540426 Var73 c545477 Var76) Var73))
||
||1. (~ (p Var73 c545477))
||2. (~ (c Var70 c545477))
||3. (p c545477 c545479)
||4. (ntpp c545478 c545477)
||5. (ec c545479 c545478)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 7
|||
|||? (p Var73 Var79)
|||
|||1. (c (f540426 Var73 c545477 Var76) Var73)
|||2. (~ (p Var73 c545477))
|||3. (~ (c Var70 c545477))
|||4. (p c545477 c545479)
|||5. (ntpp c545478 c545477)
|||6. (ec c545479 c545478)
|||
|||> ((p X Y) <-- (pp X Y))
|||=============================
|||Step 8
|||
|||? (pp Var73 Var79)
|||
|||1. (~ (p Var73 Var79))
|||2. (c (f540426 Var73 c545477 Var76) Var73)
|||3. (~ (p Var73 c545477))
|||4. (~ (c Var70 c545477))
|||5. (p c545477 c545479)
|||6. (ntpp c545478 c545477)
|||7. (ec c545479 c545478)
|||
|||> ((pp X Y) <-- (ntpp X Y))
|||=============================
|||Step 9
|||
|||? (ntpp Var73 Var79)
|||
|||1. (~ (pp Var73 Var79))
|||2. (~ (p Var73 Var79))
|||3. (c (f540426 Var73 c545477 Var76) Var73)
|||4. (~ (p Var73 c545477))
|||5. (~ (c Var70 c545477))
|||6. (p c545477 c545479)
|||7. (ntpp c545478 c545477)
|||8. (ec c545479 c545478)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (c (f540426 c545478 c545477 Var76) c545477))
||
||1. (c (f540426 c545478 c545477 Var76) c545478)
||2. (~ (p c545478 c545477))
||3. (~ (c Var70 c545477))
||4. (p c545477 c545479)
||5. (ntpp c545478 c545477)
||6. (ec c545479 c545478)
||
||> ((~ (c (f540426 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 11
||
||? (~ (p c545478 c545477))
||
||1. (c (f540426 c545478 c545477 Var76) c545477)
||2. (c (f540426 c545478 c545477 Var76) c545478)
||3. (~ (p c545478 c545477))
||4. (~ (c Var70 c545477))
||5. (p c545477 c545479)
||6. (ntpp c545478 c545477)
||7. (ec c545479 c545478)
||
||> hyp
|=============================
|Step 12
|
|? (c (f540426 c545478 Var91 Var92) c545478)
|
|1. (~ (c (f540426 c545478 Var91 Var92) c545477))
|2. (p c545477 c545479)
|3. (ntpp c545478 c545477)
|4. (ec c545479 c545478)
|
|> ((c (f540426 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 13
|
|? (~ (p c545478 Var91))
|
|1. (~ (c (f540426 c545478 Var91 Var92) c545478))
|2. (~ (c (f540426 c545478 Var91 Var92) c545477))
|3. (p c545477 c545479)
|4. (ntpp c545478 c545477)
|5. (ec c545479 c545478)
|
|> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
||=============================
||Step 14
||
||? (p c545478 Var95)
||
||1. (p c545478 Var91)
||2. (~ (c (f540426 c545478 Var91 Var92) c545478))
||3. (~ (c (f540426 c545478 Var91 Var92) c545477))
||4. (p c545477 c545479)
||5. (ntpp c545478 c545477)
||6. (ec c545479 c545478)
||
||> ((p Z X) <-- (~ (c (f540426 Z X Y) Z)))
||=============================
||Step 15
||
||? (~ (c (f540426 c545478 c545478 Var98) c545478))
||
||1. (~ (p c545478 c545478))
||2. (p c545478 Var91)
||3. (~ (c (f540426 c545478 Var91 Var92) c545478))
||4. (~ (c (f540426 c545478 Var91 Var92) c545477))
||5. (p c545477 c545479)
||6. (ntpp c545478 c545477)
||7. (ec c545479 c545478)
||
||> ((~ (c (f540426 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 16
||
||? (~ (p c545478 c545478))
||
||1. (c (f540426 c545478 c545478 Var98) c545478)
||2. (~ (p c545478 c545478))
||3. (p c545478 Var91)
||4. (~ (c (f540426 c545478 Var91 Var92) c545478))
||5. (~ (c (f540426 c545478 Var91 Var92) c545477))
||6. (p c545477 c545479)
||7. (ntpp c545478 c545477)
||8. (ec c545479 c545478)
||
||> hyp
|=============================
|Step 17
|
|? (~ (o Var91 c545478))
|
|1. (p c545478 Var91)
|2. (~ (c (f540426 c545478 Var91 Var92) c545478))
|3. (~ (c (f540426 c545478 Var91 Var92) c545477))
|4. (p c545477 c545479)
|5. (ntpp c545478 c545477)
|6. (ec c545479 c545478)
|
|> ((~ (o X Y)) <-- (ec X Y))
|=============================
|Step 18
|
|? (ec Var91 c545478)
|
|1. (o Var91 c545478)
|2. (p c545478 Var91)
|3. (~ (c (f540426 c545478 Var91 Var92) c545478))
|4. (~ (c (f540426 c545478 Var91 Var92) c545477))
|5. (p c545477 c545479)
|6. (ntpp c545478 c545477)
|7. (ec c545479 c545478)
|
|> hyp
=============================
Step 19

? (~ (c (f540426 c545478 c545479 Var92) c545479))

1. (p c545477 c545479)
2. (ntpp c545478 c545477)
3. (ec c545479 c545478)

> ((~ (c (f540426 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 20

? (~ (p c545478 c545479))

1. (c (f540426 c545478 c545479 Var92) c545479)
2. (p c545477 c545479)
3. (ntpp c545478 c545477)
4. (ec c545479 c545478)

> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
|=============================
|Step 21
|
|? (p c545478 Var109)
|
|1. (p c545478 c545479)
|2. (c (f540426 c545478 c545479 Var92) c545479)
|3. (p c545477 c545479)
|4. (ntpp c545478 c545477)
|5. (ec c545479 c545478)
|
|> ((p Z X) <-- (~ (c (f540426 Z X Y) Z)))
|=============================
|Step 22
|
|? (~ (c (f540426 c545478 c545478 Var112) c545478))
|
|1. (~ (p c545478 c545478))
|2. (p c545478 c545479)
|3. (c (f540426 c545478 c545479 Var92) c545479)
|4. (p c545477 c545479)
|5. (ntpp c545478 c545477)
|6. (ec c545479 c545478)
|
|> ((~ (c (f540426 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 23
|
|? (~ (p c545478 c545478))
|
|1. (c (f540426 c545478 c545478 Var112) c545478)
|2. (~ (p c545478 c545478))
|3. (p c545478 c545479)
|4. (c (f540426 c545478 c545479 Var92) c545479)
|5. (p c545477 c545479)
|6. (ntpp c545478 c545477)
|7. (ec c545479 c545478)
|
|> hyp
=============================
Step 24

? (~ (o c545479 c545478))

1. (p c545478 c545479)
2. (c (f540426 c545478 c545479 Var92) c545479)
3. (p c545477 c545479)
4. (ntpp c545478 c545477)
5. (ec c545479 c545478)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 25

? (ec c545479 c545478)

1. (o c545479 c545478)
2. (p c545478 c545479)
3. (c (f540426 c545478 c545479 Var92) c545479)
4. (p c545477 c545479)
5. (ntpp c545478 c545477)
6. (ec c545479 c545478)

> hyp


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c550708 c550707)) v (pp c550708 c550707))


> hypdisj
=============================
Step 3

? (pp c550708 c550707)

1. (ntpp c550708 c550707)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c550708 c550707)

1. (~ (pp c550708 c550707))
2. (ntpp c550708 c550707)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c555993 c555992)) v (p c555993 c555992))


> hypdisj
=============================
Step 3

? (p c555993 c555992)

1. (pp c555993 c555992)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c555993 c555992)

1. (~ (p c555993 c555992))
2. (pp c555993 c555992)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c561336 c561335)) v (~ (c c561334 c561336))) v (c c561334 c561335))


> hypdisj
=============================
Step 3

? (c c561334 c561335)

1. (c c561334 c561336)
2. (p c561336 c561335)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c561335)
|
|1. (~ (c c561334 c561335))
|2. (c c561334 c561336)
|3. (p c561336 c561335)
|
|> hyp
=============================
Step 5

? (c c561334 c561336)

1. (~ (c c561334 c561335))
2. (c c561334 c561336)
3. (p c561336 c561335)

> hyp


LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c566833 c566832)) v (c c566833 c566832))


> hypdisj
=============================
Step 3

? (c c566833 c566832)

1. (ec c566833 c566832)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c566833 c566832)

1. (~ (c c566833 c566832))
2. (ec c566833 c566832)

> hyp


LEMMA

From ec(x,y) and ntpp(y,z), x is connected to z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp y z)) => (c x z)))))


> revsk
=============================
Step 2

? (((~ (ec c572388 c572387)) v (~ (ntpp c572387 c572386))) v (c c572388 c572386))


> hypdisj
=============================
Step 3

? (c c572388 c572386)

1. (ntpp c572387 c572386)
2. (ec c572388 c572387)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var30 c572386)
|
|1. (~ (c c572388 c572386))
|2. (ntpp c572387 c572386)
|3. (ec c572388 c572387)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 5
|
|? (pp Var30 c572386)
|
|1. (~ (p Var30 c572386))
|2. (~ (c c572388 c572386))
|3. (ntpp c572387 c572386)
|4. (ec c572388 c572387)
|
|> ((pp X Y) <-- (ntpp X Y))
|=============================
|Step 6
|
|? (ntpp Var30 c572386)
|
|1. (~ (pp Var30 c572386))
|2. (~ (p Var30 c572386))
|3. (~ (c c572388 c572386))
|4. (ntpp c572387 c572386)
|5. (ec c572388 c572387)
|
|> hyp
=============================
Step 7

? (c c572388 c572387)

1. (~ (c c572388 c572386))
2. (ntpp c572387 c572386)
3. (ec c572388 c572387)

> ((c X Y) <-- (ec X Y))
=============================
Step 8

? (ec c572388 c572387)

1. (~ (c c572388 c572387))
2. (~ (c c572388 c572386))
3. (ntpp c572387 c572386)
4. (ec c572388 c572387)

> hyp


LEMMA

Because ntpp(y,z) is internal and x is connected to y, x overlaps z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp y z)) => (o x z)))))


> revsk
=============================
Step 2

? (((~ (ec c578099 c578098)) v (~ (ntpp c578098 c578097))) v (o c578099 c578097))


> hypdisj
=============================
Step 3

? (o c578099 c578097)

1. (ntpp c578098 c578097)
2. (ec c578099 c578098)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c578099 c578097)
|
|1. (~ (o c578099 c578097))
|2. (ntpp c578098 c578097)
|3. (ec c578099 c578098)
|
|> ((c X Z) <-- (ec X Y) (ntpp Y Z))
||=============================
||Step 5
||
||? (ec c578099 Var33)
||
||1. (~ (c c578099 c578097))
||2. (~ (o c578099 c578097))
||3. (ntpp c578098 c578097)
||4. (ec c578099 c578098)
||
||> hyp
|=============================
|Step 6
|
|? (ntpp c578098 c578097)
|
|1. (~ (c c578099 c578097))
|2. (~ (o c578099 c578097))
|3. (ntpp c578098 c578097)
|4. (ec c578099 c578098)
|
|> hyp
=============================
Step 7

? (~ (ec c578099 c578097))

1. (~ (o c578099 c578097))
2. (ntpp c578098 c578097)
3. (ec c578099 c578098)

> ((~ (ec Y X)) <-- (ntpp Z X) (ec Y Z))
|=============================
|Step 8
|
|? (ntpp Var38 c578097)
|
|1. (ec c578099 c578097)
|2. (~ (o c578099 c578097))
|3. (ntpp c578098 c578097)
|4. (ec c578099 c578098)
|
|> hyp
=============================
Step 9

? (ec c578099 c578098)

1. (ec c578099 c578097)
2. (~ (o c578099 c578097))
3. (ntpp c578098 c578097)
4. (ec c578099 c578098)

> hyp


LEMMA

Overlap together with failure of converse parthood yields po(x,z) or pp(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp y z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? (((~ (ec c583966 c583965)) v (~ (ntpp c583965 c583964))) v ((po c583966 c583964) v (pp c583966 c583964)))


> hypdisj
=============================
Step 3

? (pp c583966 c583964)

1. (~ (po c583966 c583964))
2. (ntpp c583965 c583964)
3. (ec c583966 c583965)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c583966 c583964)
|
|1. (~ (pp c583966 c583964))
|2. (~ (po c583966 c583964))
|3. (ntpp c583965 c583964)
|4. (ec c583966 c583965)
|
|> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
|||=============================
|||Step 5
|||
|||? (o c583966 c583964)
|||
|||1. (~ (p c583966 c583964))
|||2. (~ (pp c583966 c583964))
|||3. (~ (po c583966 c583964))
|||4. (ntpp c583965 c583964)
|||5. (ec c583966 c583965)
|||
|||> ((o X Z) <-- (ec X Y) (ntpp Y Z))
||||=============================
||||Step 6
||||
||||? (ec c583966 Var43)
||||
||||1. (~ (o c583966 c583964))
||||2. (~ (p c583966 c583964))
||||3. (~ (pp c583966 c583964))
||||4. (~ (po c583966 c583964))
||||5. (ntpp c583965 c583964)
||||6. (ec c583966 c583965)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (ntpp c583965 c583964)
|||
|||1. (~ (o c583966 c583964))
|||2. (~ (p c583966 c583964))
|||3. (~ (pp c583966 c583964))
|||4. (~ (po c583966 c583964))
|||5. (ntpp c583965 c583964)
|||6. (ec c583966 c583965)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (p c583964 c583966))
||
||1. (~ (p c583966 c583964))
||2. (~ (pp c583966 c583964))
||3. (~ (po c583966 c583964))
||4. (ntpp c583965 c583964)
||5. (ec c583966 c583965)
||
||> ((~ (p Z X)) <-- (ec X Y) (ntpp Y Z))
|||=============================
|||Step 9
|||
|||? (ec c583966 Var48)
|||
|||1. (p c583964 c583966)
|||2. (~ (p c583966 c583964))
|||3. (~ (pp c583966 c583964))
|||4. (~ (po c583966 c583964))
|||5. (ntpp c583965 c583964)
|||6. (ec c583966 c583965)
|||
|||> hyp
||=============================
||Step 10
||
||? (ntpp c583965 c583964)
||
||1. (p c583964 c583966)
||2. (~ (p c583966 c583964))
||3. (~ (pp c583966 c583964))
||4. (~ (po c583966 c583964))
||5. (ntpp c583965 c583964)
||6. (ec c583966 c583965)
||
||> hyp
|=============================
|Step 11
|
|? (~ (po c583966 c583964))
|
|1. (~ (p c583966 c583964))
|2. (~ (pp c583966 c583964))
|3. (~ (po c583966 c583964))
|4. (ntpp c583965 c583964)
|5. (ec c583966 c583965)
|
|> hyp
=============================
Step 12

? (~ (p c583964 c583966))

1. (~ (pp c583966 c583964))
2. (~ (po c583966 c583964))
3. (ntpp c583965 c583964)
4. (ec c583966 c583965)

> ((~ (p Z X)) <-- (ec X Y) (ntpp Y Z))
|=============================
|Step 13
|
|? (ec c583966 Var54)
|
|1. (p c583964 c583966)
|2. (~ (pp c583966 c583964))
|3. (~ (po c583966 c583964))
|4. (ntpp c583965 c583964)
|5. (ec c583966 c583965)
|
|> hyp
=============================
Step 14

? (ntpp c583965 c583964)

1. (p c583964 c583966)
2. (~ (pp c583966 c583964))
3. (~ (po c583966 c583964))
4. (ntpp c583965 c583964)
5. (ec c583966 c583965)

> hyp


LEMMA

Proper part splits into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c590097 c590096)) v ((tpp c590097 c590096) v (ntpp c590097 c590096)))


> hypdisj
=============================
Step 3

? (ntpp c590097 c590096)

1. (~ (tpp c590097 c590096))
2. (pp c590097 c590096)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f584079 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c590097 c590096)
|
|1. (~ (ntpp c590097 c590096))
|2. (~ (tpp c590097 c590096))
|3. (pp c590097 c590096)
|
|> hyp
=============================
Step 5

? (~ (ec (f584079 c590097 c590096 Var32) c590097))

1. (~ (ntpp c590097 c590096))
2. (~ (tpp c590097 c590096))
3. (pp c590097 c590096)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c590097 Var36)
||
||1. (ec (f584079 c590097 c590096 Var32) c590097)
||2. (~ (ntpp c590097 c590096))
||3. (~ (tpp c590097 c590096))
||4. (pp c590097 c590096)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f584079 c590097 c590096 Var32) c590096)
|
|1. (ec (f584079 c590097 c590096 Var32) c590097)
|2. (~ (ntpp c590097 c590096))
|3. (~ (tpp c590097 c590096))
|4. (pp c590097 c590096)
|
|> ((ec (f584079 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c590097 c590096))
||
||1. (~ (ec (f584079 c590097 c590096 Var32) c590096))
||2. (ec (f584079 c590097 c590096 Var32) c590097)
||3. (~ (ntpp c590097 c590096))
||4. (~ (tpp c590097 c590096))
||5. (pp c590097 c590096)
||
||> hyp
|=============================
|Step 9
|
|? (pp c590097 c590096)
|
|1. (~ (ec (f584079 c590097 c590096 Var32) c590096))
|2. (ec (f584079 c590097 c590096 Var32) c590097)
|3. (~ (ntpp c590097 c590096))
|4. (~ (tpp c590097 c590096))
|5. (pp c590097 c590096)
|
|> hyp
=============================
Step 10

? (~ (tpp c590097 c590096))

1. (ec (f584079 c590097 c590096 Var32) c590097)
2. (~ (ntpp c590097 c590096))
3. (~ (tpp c590097 c590096))
4. (pp c590097 c590096)

> hyp


LEMMA

Get o(x,z), then refine to po(x,z) or pp(x,z); split pp into tpp(x,z) or ntpp(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp y z)) => (((po x z) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (ec c596381 c596380)) v (~ (ntpp c596380 c596379))) v (((po c596381 c596379) v (tpp c596381 c596379)) v (ntpp c596381 c596379)))


> hypdisj
=============================
Step 3

? (ntpp c596381 c596379)

1. (~ (tpp c596381 c596379))
2. (~ (po c596381 c596379))
3. (ntpp c596380 c596379)
4. (ec c596381 c596380)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c596381 c596379)
|
|1. (~ (ntpp c596381 c596379))
|2. (~ (tpp c596381 c596379))
|3. (~ (po c596381 c596379))
|4. (ntpp c596380 c596379)
|5. (ec c596381 c596380)
|
|> ((pp Y Z) <-- (ec Y X) (ntpp X Z) (~ (po Y Z)))
|||=============================
|||Step 5
|||
|||? (ec c596381 Var30)
|||
|||1. (~ (pp c596381 c596379))
|||2. (~ (ntpp c596381 c596379))
|||3. (~ (tpp c596381 c596379))
|||4. (~ (po c596381 c596379))
|||5. (ntpp c596380 c596379)
|||6. (ec c596381 c596380)
|||
|||> hyp
||=============================
||Step 6
||
||? (ntpp c596380 c596379)
||
||1. (~ (pp c596381 c596379))
||2. (~ (ntpp c596381 c596379))
||3. (~ (tpp c596381 c596379))
||4. (~ (po c596381 c596379))
||5. (ntpp c596380 c596379)
||6. (ec c596381 c596380)
||
||> hyp
|=============================
|Step 7
|
|? (~ (po c596381 c596379))
|
|1. (~ (pp c596381 c596379))
|2. (~ (ntpp c596381 c596379))
|3. (~ (tpp c596381 c596379))
|4. (~ (po c596381 c596379))
|5. (ntpp c596380 c596379)
|6. (ec c596381 c596380)
|
|> hyp
=============================
Step 8

? (~ (tpp c596381 c596379))

1. (~ (ntpp c596381 c596379))
2. (~ (tpp c596381 c596379))
3. (~ (po c596381 c596379))
4. (ntpp c596380 c596379)
5. (ec c596381 c596380)

> hyp
